Div(a;n;q) == n * q  a < n * (q+1) 

latex

Up	int 2, int 2
Wellformedness Lemmas	div nrel wf, div nrel wf
Definitions	i  j < k, n * m, n+m, #$n
FDL editor aliases	div_nrel